perm filename SUBSUM.NEW[1,JRA] blob
sn#005866 filedate 1972-09-25 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP ATTEMPT
00400 (LAMBDA(L S C)
00500 (PROG (NEWNAME SUPPORT
00600 UNITPF
00700 LCL
00800 LVL
00900 CNT
01000 XYZ2
01100 LSTCLS
01200 LLST
01300 Z1
01400 MERGE
01500 ORDER
01600 DEBUG
01700 DEPTH
01800 LENGTH
01900 ANCESTRY
02000 STRATEGY
02100 STRAT
02200 PMODEL
02300 NMODEL
02400 PFLG
02500 EQUAL
02600 PDEPTH
02700 DLIST
02800 XYZ
02900 XYZ1
03000 COND
03100 Z
03200 UNAXP
03300 UNAXN
03400 SAT
03500 EXTERM
03600 EE
03700 EE1
03800 XX
03900 CLAUSES
04000 SUBCLAUSES
04100 COUNT
04200 SLENGTH
04300 ORDLST
04400 OCLIST)
04500 (SETQ NEWNAME (LIST (LIST NIL)))
04600 (SETORD (CAR L) (CDR L))
04700 (SETQ Z (MINIMIZE (CAR L)))
04800 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
04900 (SETQ COND C)
05000 (SETQ XYZ2 Z)
05100 (SETQ LVL 1)
05200 (SETQ COUNT 0)
05300 (SETQ Z (UNITPN XYZ2))
05400 (SETQ UNAXP (CAR Z))
05500 (SETQ UNAXN (CDR Z))
05600 (SETQ CLAUSES XYZ2)
05700 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
05800 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
05900 (T (SETQ SUBCLAUSES CLAUSES)))
06000 (SETQ LCL (LAST CLAUSES))
06100 (SETQ LSTCLS LCL)
06200 (COND (ANCESTRY (GO AA)))
06300 (SETQ XX (CONS CLAUSES CLAUSES))
06400 (SETQ EE CLAUSES)
06500 (SETQ EE1 (LAST EE))
06600 (SETQ CNT (LENGTH XYZ2))
06700 BB (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
06800 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (CONS (QUOTE NOPROOF) (CONS CLAUSES STRAT))))
06900 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
07000 (EVAL
07100 (LIST (QUOTE OUTC)
07200 (LIST (QUOTE OUTPUT) (QUOTE PRF) (QUOTE DSK:) FILENAM)
07300 NIL)))
07400 (QUERY)
07500 (PROOF LHP RHP)
07600 (OUTC Z T)
07700 (RETURN Z1))
07800 (T (RETURN Z1)))
07900 AA (SETQ XYZ XYZ2)
08000 (SETQ EE CLAUSES)
08100 (SETQ EE1 (LAST CLAUSES))
08200 CC (SETQ LLST (CONS (CAR XYZ) LLST))
08300 (SETQ XYZ (CDR XYZ))
08400 (COND (XYZ (GO CC)) (T (GO BB)))))
08500 EXPR)
08600
08700 (DEFPROP EDIT
08800 (LAMBDA(U Z)
08900 (PROG (RES1 U1 U4 U5)
09000 ED4 (COND ((NULL Z) (RETURN RES1)))
09100 (SETQ U4 (CAR Z))
09200 (SETQ U5 (CDR U4))
09300 (COND ((OR (GREATERP (NUM U4) LENGTH) (GREATERP (DEPTH U5) DEPTH)) (GO ED2)))
09400 (SETQ U1 SUBCLAUSES)
09500 ED1
09600 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
09700 ED6 (SETQ U1 (CDR U1))
09800 (COND (U1 (GO ED1)))
09900 (SETQ U1 (CDR Z))
10000 (COND ((NULL U1) (GO ED5)))
10100 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
10200 ED7 (SETQ U1 (CDR U1))
10300 (COND (U1 (GO ED3)))
10400 ED5 (SETQ RES1 (CONS U4 RES1))
10500 ED2 (SETQ Z (CDR Z))
10600 (GO ED4)))
10700 EXPR)
10800
10900 (DEFPROP SUBSUME
11000 (LAMBDA(C D)
11100 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
11200 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
11300 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
11400 (T NIL)))
11500 EXPR)